#ifndef __RESTART_KERNEL_H__
#define __RESTART_KERNEL_H__

#include "solver_function.h"
#include "vec.h"

// TODO: Sort leanrt clause by their size and do subsumption.

// Only one thread, one block
__global__ void
//__launch_bounds__ ( __threadsPerBlock2, 1 )
kernel_restart_global_settings( void )
{
	int tId = threadIdx.x;

	__shared__ int size;
	__shared__ int learntSize;

	if ( tId == 0 )
	{
		size = atomicMax( __dev_clausePtrIndexSize, 0 );
		learntSize = size - __dev_claNumber;
#ifdef NO_IDLE_BLOCK
		__dev_hasResult = 0;
#endif
#ifdef HALF_IDLE_BLOCK
		__dev_idleBlockCount = 0;
#endif
		if ( size < __clausePtrIndexCapacity )
		{
			__dev_conflictLimit += __dev_conflictLimit + (__dev_conflictLimit >> 1);
#ifndef KEEP_LEARNT_CLAUSE
			__dev_learntClauseLimit += __dev_learntClauseLimit + (__dev_learntClauseLimit >> 1);
#endif
		}
		__dev_claActivityIncreaseDelta *= __dev_claActivityIncreaseRate;
		__dev_decreaseClauseActivity = 0;
#ifdef DEBUG_CRITICAL
	#ifdef KEEP_LEARNT_CLAUSE
		printf( "kernel_restart_global_settings(): __dev_conflictLimit = %d, __dev_claActivityIncreaseDelta = %f\n", __dev_conflictLimit, __dev_claActivityIncreaseDelta );
	#else
		printf( "kernel_restart_global_settings(): __dev_conflictLimit = %d, __dev_learntClauseLimit = %d, __dev_claActivityIncreaseDelta = %f\n", __dev_conflictLimit, __dev_learntClauseLimit, __dev_claActivityIncreaseDelta );
	#endif
#endif
	} // if ( tId == 0 )
	__threadfence_block();

	for ( int i = tId; i < learntSize; i += __threadsPerBlock2 )
	{
		int index = i + __dev_claNumber;
		Clause* c = get_clausePtrIndex( index );
#ifdef ASSERT
		if ( c == NULL )
		{ printf("kernel_restart_global_settings(): tId = %d: c = NULL, index = %d\n", tId, index ); }
#endif
		c->set_index(index);
	}
#ifdef ASSERT
	for ( int i = tId; i < size; ++i )
	{
		if ( get_clausePtrIndex(i) == NULL )
		{ printf("kernel_restart_global_settings(): Assertion failed: __dev_clausePtrIndex[%d] == NULL, szie = %d\n", i, size ); }
	}
#endif

	return;
}

__global__ void
//__launch_bounds__ ( __threadsPerBlock, __minBlocksPerMultiprocessor )
kernel_restart_block_settings( void )
{
	int tId = threadIdx.x;
	int bId = blockIdx.x;

	__shared__ int size;

	if ( get_satResult( bId ).convert_to_int() != __LBOOL_UNDEF_INT )
	{
		if ( bId != 0 )
		{
			// DO NOT deallocate block 0's watch list, it is used in generating global table during restart.
			for ( int i = tId; i < __dev_litNumber; i += __threadsPerBlock )
			{ get_watchList( get_watchListPtr( bId ), i )->clear( true ); }
		}
		return;
	}

	__shared__ Lbool*			tVarAssignment;
	__shared__ Lit**			tWatchPointer;
	__shared__ Vec <Clause*>*	tWatchList;

	if ( tId == 0 )
	{
		tVarAssignment = (Lbool*)( (char*)__dev_varAssignment + bId * __dev_varAssignmentPitch );
		tWatchPointer =  (Lit**)( (char*)__dev_watchPointer + bId * __dev_watchPointerPitch );
		tWatchList = get_watchListPtr( bId );
		size = *__dev_clausePtrIndexSize;
	}
	__threadfence_block();

#ifdef ASSERT
	for ( int i = tId; i < size; ++i )
	{
		if ( get_clausePtrIndex(i) == NULL )
		{ printf("kernel_restart_block_settings(): Assertion failed: __dev_clausePtrIndex[%d] == NULL, size = %d\n", i, size ); }
	}
#endif

	for ( int i = tId; i < __dev_varNumber; i += __threadsPerBlock )
	{ set_varAssignment( tVarAssignment, i, Lbool() ); }
	__threadfence_block();

	for ( int i = tId; i < __dev_litNumber; i += __threadsPerBlock )
	{ get_watchList( tWatchList, i )->clear(); }
	__threadfence_block();
	__syncthreads();

	// Initialize watch pointers in this block.
	for ( int i = tId; i < size; i += __threadsPerBlock )
	{
		Clause* c = get_clausePtrIndex(i);
#ifdef ASSERT
			if ( c == NULL )
			{ printf("kernel_restart_block_settings: tId = %d bId #%d: c = NULL, i = %d\n", tId, bId, i ); }
#endif
		set_watchPointer( tWatchPointer, (i << 1), c->data_pointer(0) );
		set_watchPointer( tWatchPointer, ((i << 1) + 1), c->data_pointer(1) );
	}
	__threadfence_block();

	// Initilize watch list.
	for ( int i = tId; i < __dev_litNumber; i += __threadsPerBlock )
	{
		for ( int j = 0; j < size; ++j )
		{
			if ( get_watchPointer( tWatchPointer, (j << 1) )->index() == i )
			{
				get_watchList( tWatchList, i )->push_back( get_clausePtrIndex(j) );
#ifdef DEBUG_CUDASAT
				if ( i == 22 )
				{
					printf("(1) i = %d, j = %d, clause index = %d\n", i, j, get_clausePtrIndex(j)->index() );
					for ( int k = 0; k < get_clausePtrIndex(j)->size(); ++k )
					{
						printf("(1) i = %d, j = %d, k = %d, Lit #%d\n", i, j, k, get_clausePtrIndex(j)->data(k).index() );
					}
				}
#endif
			}

			if ( get_watchPointer( tWatchPointer, ((j << 1) + 1) )->index() == i )
			{
				get_watchList( tWatchList, i )->push_back( get_clausePtrIndex(j) );
#ifdef DEBUG_CUDASAT
				if ( i == 22 )
				{
					printf("(2) i = %d, j = %d, \n", i, j );
					for ( int k = 0; k < get_clausePtrIndex(j)->size(); ++k )
					{
						printf("(2) i = %d, j = %d, k = %d, Lit #%d\n", i, j, k, get_clausePtrIndex(j)->data(k).index() );
					}
				}
#endif
			}
#ifdef ASSERT
			if ( (*get_watchPointer( tWatchPointer, (j << 1) )) == (*get_watchPointer( tWatchPointer, ((j << 1) + 1) )) )
			{ printf( "kernel_restart_block_settings(): Assertion failed: tId #%d bId #%d: initilizing two watch pointers in the same clause points to the same literal #%d.\n", tId, bId, i ); }
#endif
		}
	}

#ifdef ASSERT
	__threadfence_block();

	for ( int i = tId; i < __dev_litNumber; i += __threadsPerBlock )
	{
		int listSize = get_watchList( tWatchList, i )->size();

		for ( int j = 0; j < listSize; ++j )
		{
			int index = get_watchList( tWatchList, i )->at(j)->index() << 1;

			if ( (get_watchPointer( tWatchPointer, index )->index() != i)
				&& (get_watchPointer( tWatchPointer, (index + 1) )->index() != i) )
			{
				printf( "kernel_restart_block_settings(): Assertion failed: tId #%d bId #%d: Watch list of Lit #%d has other Lit #%d and #%d.\n",
					tId, bId, i,
					get_watchPointer( tWatchPointer, index )->index(),
					get_watchPointer( tWatchPointer, (index + 1) )->index() );
			}
		}
	}
#endif

	return;
}

// One block. This should be called before sorting.
__global__ void
//__launch_bounds__ ( __threadsPerBlock2, 1 )
kernel_reduce_learnt_clause( void )
{
	int tId = threadIdx.x;

	__shared__ int size;
	__shared__ int newSize;
	__shared__ int unitSize;
	__shared__ int learntSize;
	__shared__ int unitRemoveCount;
	__shared__ int duplicatedCount;

	if ( tId == 0 )
	{
		unitRemoveCount = 0;
		duplicatedCount = 0;
		size = atomicMax( __dev_clausePtrIndexSize, 0 );
		unitSize = atomicMax( &__dev_unitClauseLitSize, 0 );
		learntSize = size - __dev_claNumber;
#ifdef DEBUG_CRITICAL
		printf("kernel_reduce_learnt_clause(): __dev_claNumber = %d, size = %d: unitSize = %d, learntSize = %d\n", __dev_claNumber, size, unitSize, learntSize );
#endif

#ifdef KEEP_LEARNT_CLAUSE
		if ( size >= __clausePtrIndexCapacity )
#else
		if ( learntSize > __dev_learntClauseLimit )
#endif
		{ newSize = __clausePtrIndexCapacity - (learntSize >> 1); }
		else
		{ newSize = size; }
	}
	__threadfence_block();

	if ( newSize < size )
	{
		for ( int i = tId; i < size; i += __threadsPerBlock2 )
		{
			int index = i + newSize;
			Clause* cla = get_clausePtrIndex( index );

			if ( cla != NULL )
			{
				delete cla;
				set_clausePtrIndex( index, NULL );
			}
		}

		if ( tId == 0 )
		{ atomicCAS( __dev_clausePtrIndexSize, size, newSize ); }
		__threadfence_block();
	}

	if ( tId == 0 )
	{
		size = atomicMax( __dev_clausePtrIndexSize, 0 );
		learntSize = size - __dev_claNumber;
#ifdef DEBUG_CRITICAL
		printf( "kernel_reduce_learnt_clause(): *__dev_clausePtrIndexSize = %d, __dev_claNumber = %d, learntSize = %d\n", (*__dev_clausePtrIndexSize), __dev_claNumber, learntSize );
#endif
#ifdef ASSERT
		if ( (*__dev_clausePtrIndexSize) < __dev_claNumber )
		{ printf( "Assertion failed: *__dev_clausePtrIndexSize = %d < __dev_claNumber = %d\n", (*__dev_clausePtrIndexSize), __dev_claNumber ); }
#endif
	}
	__threadfence_block();

	if ( __dev_decreaseClauseActivity > 0 )
	{
		for ( int i = tId; i < size; i += __threadsPerBlock2 )
		{ set_clauseActivityKey( i, (get_clauseActivityKey(i) * 1e-20) ); }
	}

	// Building a learnt clause list table for literals vs. clauses.
	// Borrowing the tWatchList of block 0.
	for ( int i = tId; i < __dev_litNumber; i += __threadsPerBlock2 )
	{ get_watchList( get_watchListPtr(0), i )->clear(); }
	__threadfence_block();

	for ( int i = tId; i < __dev_litNumber; i += __threadsPerBlock2 )
	{
		Vec <Clause*>* list = get_watchList( get_watchListPtr(0), i );
#ifdef ASSERT
		if ( list == NULL )
		{ printf("kernel_reduce_learnt_clause(): tId = %d: list = NULL, i = %d\n", tId, i ); }
#endif
		for ( int j = __dev_claNumber; j < size; ++j )
		{
			Clause* c = get_clausePtrIndex(j);
#ifdef ASSERT
			if ( c == NULL )
			{ printf("kernel_reduce_learnt_clause(): tId = %d: c = NULL, i = %d, j = %d\n", tId, i, j ); }
#endif
			int size2 = c->size();

			for ( int k = 0; k < size2; ++k )
			{
				if ( (c->data( k )).index() == i )
				{ list->push_back( c ); break; }
			}
		}
	}
	__threadfence_block();

	// TODO: read level 0 record and add them into unit clauses. Pay attention to conflicts (UNSAT).

	for ( int i = tId; i < unitSize; i += __threadsPerBlock2 )
	{
		Vec <Clause*>* list = get_watchList( get_watchListPtr(0), get_unitClauseLit(i).index() );
		int listSize = list->size();

		// Remove clauses with one true literal.
		for ( int j = 0; j < listSize; ++j )
		{
			(list->at(j))->set_remove();
			atomicAdd( &unitRemoveCount, 1 );
		}
	}
	__threadfence_block();

#ifdef DEBUG_CRITICAL
	if ( tId == 0 )
	{ printf( "kernel_reduce_learnt_clause(): unitRemoveCount = %d (inaccurate due to parallelization)\n", unitRemoveCount ); }
#endif

	// Remove duplicated learnt clauses.
	for ( int i = (tId + __dev_claNumber); i < size; i += __threadsPerBlock2 )
	{
		Clause* c1 = get_clausePtrIndex(i);
#ifdef ASSERT
		if ( c1 == NULL )
		{ printf("kernel_reduce_learnt_clause(): tId = %d: c1 = NULL\n", tId ); }
#endif
		if ( c1->get_remove() == true )
		{ continue; }

		unsigned int hash = c1->get_hash();

		for ( int j = (i + 1); j < size; ++j )
		{
			Clause* c2 = get_clausePtrIndex(j);
#ifdef ASSERT
			if ( c2 == NULL )
			{ printf("kernel_reduce_learnt_clause(): tId = %d: c2 = NULL, i = %d, j = %d\n", tId, i, j ); }
#endif
			if ( (c2->get_remove() == true) || (c2->get_hash() != hash) || (c1->size() != c2->size()) )
			{ continue; }

			volatile bool remove = true;

			for ( int k = 0; k < c1->size(); ++k )
			{
				volatile bool found = false;
				Lit lit = c1->data(k);

				for ( int m = 0; m < c2->size(); ++m )
				{
					if ( c2->data(m) == lit )
					{ found = true; break; }
				}

				if ( found == false )
				{ remove = false; break; }
			}

			if ( remove == true )
			{
				c2->set_remove();
				atomicAdd( &duplicatedCount, 1 );
			}
		}
	}
	__threadfence_block();

#ifdef DEBUG_CRITICAL
	if ( tId == 0 )
	{ printf( "kernel_reduce_learnt_clause(): duplicatedCount = %d\n", duplicatedCount ); }
#endif

#ifdef ASSERT
	for ( int i = tId; i < size; i += __threadsPerBlock2 )
	{
		if ( get_clausePtrIndex(i) == NULL )
		{ printf("kernel_reduce_learnt_clause(): Assertion failed: __dev_clausePtrIndex[%d] == NULL, size = %d\n", i, size ); }
	}

	for ( int i = tId; i < size; i += __threadsPerBlock2 )
	{
		Clause* c1 = get_clausePtrIndex(i);

		for ( int j = (i + 1); j < size; ++j )
		{
			Clause* c2 = get_clausePtrIndex(j);

			if ( c1 == c2 )
			{ printf("kernel_reduce_learnt_clause(): Assertion failed: duplicated clause pointers, i = %d, j = %d, c1 clause index = %d, c2 clause index = %d\n", i, j, c1->index(), c2->index() ); }
		}
	}
#endif

	if ( tId == 0 )
	{
		volatile int newSize = size;
#ifdef DEBUG_CRITICAL
		printf("kernel_reduce_learnt_clause(): newSize = %d\n", newSize );
#endif
		volatile int index = __dev_claNumber;
		volatile int removeCount = 0;

		while ( index < newSize )
		{
			Clause* cla = get_clausePtrIndex( index );
#ifdef ASSERT
			if ( cla == NULL )
			{ printf("kernel_reduce_learnt_clause(): Assertion failed: (1) cla == NULL, index = %d, newSize = %d\n", index, newSize ); }
#endif
			while ( cla->get_remove() == true )
			{
				delete cla;
				++removeCount;
				--newSize;
				set_clausePtrIndex( index, get_clausePtrIndex( newSize ) );
				cla = get_clausePtrIndex( newSize );
#ifdef ASSERT
				if ( cla == NULL )
				{ printf("kernel_reduce_learnt_clause(): Assertion failed: (2) cla == NULL, index = %d, newSize = %d\n", index, newSize ); }
#endif
				set_clausePtrIndex( newSize, NULL );
				__threadfence_block();
				if ( index == newSize )
				{ break; }
			}
			++index;
		}

#ifdef DEBUG_CRITICAL
		printf( "kernel_reduce_learnt_clause(): Simplify learnt clauses. removeCount = %d, newSize = %d, learntSize = %d\n", removeCount, newSize, (newSize - __dev_claNumber) );
#endif
		atomicExch( __dev_clausePtrIndexSize, newSize );
	}
	__threadfence_block();

#ifdef DEBUG_CRITICAL
	if ( tId == 0 )
	{ printf("kernel_reduce_learnt_clause(): *__dev_clausePtrIndexSize = %d\n", (*__dev_clausePtrIndexSize) ); }
#endif

	return;
}

#endif /* __RESTART_KERNEL_H__ */
